more from this thinker
|
more from this text
Single Idea 13146
[filed under theme 4. Formal Logic / D. Modal Logic ML / 2. Tools of Modal Logic / c. Derivation rules of ML
]
Full Idea
System B symmetric rules (also for S5): a) if σ.n □X then σ X b) if σ.n ¬◊X then σ ¬X [where n is a world which already occurs]
Gist of Idea
B symmetric: a) if σ.n □X then σ X b) if σ.n ¬◊X then σ ¬X [n occurs]
Source
M Fitting/R Mendelsohn (First-Order Modal Logic [1998], 2.3)
Book Ref
Fitting,M/Mendelsohn,R: 'First-Order Modal Logic' [Synthese 1998], p.52
The
15 ideas
with the same theme
[rules which are allowed in various modal logics]:
|
9740
|
If a proposition is possibly true in a world, it is true in some world accessible from that world
[Fitting/Mendelsohn]
|
|
9739
|
If a proposition is necessarily true in a world, it is true in all worlds accessible from that world
[Fitting/Mendelsohn]
|
|
13137
|
Conj: a) if σ X∧Y then σ X and σ Y b) if σ ¬(X∧Y) then σ ¬X or σ ¬Y
[Fitting/Mendelsohn]
|
|
13140
|
Bicon: a)if σ(X↔Y) then σ(X→Y) and σ(Y→X) b) [not biconditional, one or other fails]
[Fitting/Mendelsohn]
|
|
13138
|
Disj: a) if σ ¬(X∨Y) then σ ¬X and σ ¬Y b) if σ X∨Y then σ X or σ Y
[Fitting/Mendelsohn]
|
|
13143
|
Universal: a) if σ ¬◊X then σ.m ¬X b) if σ □X then σ.m X [m exists]
[Fitting/Mendelsohn]
|
|
13142
|
Existential: a) if σ ◊X then σ.n X b) if σ ¬□X then σ.n ¬X [n is new]
[Fitting/Mendelsohn]
|
|
13141
|
Negation: if σ ¬¬X then σ X
[Fitting/Mendelsohn]
|
|
13139
|
Implic: a) if σ ¬(X→Y) then σ X and σ ¬Y b) if σ X→Y then σ ¬X or σ Y
[Fitting/Mendelsohn]
|
|
13144
|
T reflexive: a) if σ □X then σ X b) if σ ¬◊X then σ ¬X
[Fitting/Mendelsohn]
|
|
13148
|
4r rev-trans: a) if σ.n □X then σ □X b) if σ.n ¬◊X then σ ¬◊X [n occurs]
[Fitting/Mendelsohn]
|
|
13147
|
4 transitive: a) if σ □X then σ.n □X b) if σ ¬◊X then σ.n ¬◊X [n occurs]
[Fitting/Mendelsohn]
|
|
13146
|
B symmetric: a) if σ.n □X then σ X b) if σ.n ¬◊X then σ ¬X [n occurs]
[Fitting/Mendelsohn]
|
|
13145
|
D serial: a) if σ □X then σ ◊X b) if σ ¬◊X then σ ¬□X
[Fitting/Mendelsohn]
|
|
13149
|
S5: a) if n ◊X then kX b) if n ¬□X then k ¬X c) if n □X then k X d) if n ¬◊X then k ¬X
[Fitting/Mendelsohn]
|